Require Export List.
Require Export Matrix.Mat_def.
Import ListNotations.

Section Mat_make.
Variable A :Set.

Definition ex1_cond1 : length [1;2] = 2%nat. 
simpl. apply eq_refl. Qed.

Definition ex1_cond1' : height [[1;2];[1;2]] = 2%nat := eq_refl.
(*
Definition ex2_cond2 n (dl:list (list A)) : 
   width dl n. := conj eq_refl (conj eq_refl I).
*)



Definition mkMat_dl m0 n0 (dl:list (list A))(H1:height dl = m0)
  (H2:width dl n0):=
  mkMat A m0 n0 dl H1 H2.

Definition mkMat_1_1' (a:A):= [[a]].

Lemma mkMat_1_1_cond2 : forall a ,
  width (mkMat_1_1' a) 1.
Proof. simpl. auto. Qed.
Definition mkMat_1_1(a:A):=
  mkMat A  1 1 
  (mkMat_1_1' a)
  eq_refl
  (mkMat_1_1_cond2 a).


Definition mkMat_1_2' (a b:A):= [[a;b]].

Lemma mkMat_1_2_cond2 : forall a b,
  width (mkMat_1_2' a b) 2.
Proof. simpl. auto. Qed.
Definition mkMat_1_2(a b:A):=
  mkMat A  1 2 
  (mkMat_1_2' a b)
  eq_refl
  (mkMat_1_2_cond2 a b).



Definition mkMat_2_1' (a b:A):= [[a];[b]].
Lemma mkMat_2_1_cond2 : forall a b,
  width (mkMat_2_1' a b) 1.
Proof. simpl. auto. Qed.
Definition mkMat_2_1(a b:A):=
  mkMat A  2 1 
  (mkMat_2_1' a b)
  eq_refl
  (mkMat_2_1_cond2 a b).

Definition mkMat_2_2' (a b c d:A):= [[a;b];[c;d]].
Lemma mkMat_2_2_cond2 : forall a b c d,
  width (mkMat_2_2' a b c d) 2.
Proof. simpl. auto. Qed.
Definition mkMat_2_2(a b c d:A):=
  mkMat A  2 2 
  (mkMat_2_2' a b c d)
  eq_refl
  (mkMat_2_2_cond2 a b c d).

Definition mkMat_2_4' (a1 a2 a3 a4 a5 a6 a7 a8:A):=
   [[a1;a2;a3;a4];[a5;a6;a7;a8]].
Lemma mkMat_2_4_cond2 : forall a1 a2 a3 a4 a5 a6 a7 a8,
  width (mkMat_2_4' a1 a2 a3 a4 a5 a6 a7 a8) 4.
Proof. simpl. auto. Qed.
Definition mkMat_2_4(a1 a2 a3 a4 a5 a6 a7 a8:A):=
  mkMat A  2 4 
  (mkMat_2_4' a1 a2 a3 a4 a5 a6 a7 a8)
  eq_refl
  (mkMat_2_4_cond2 a1 a2 a3 a4 a5 a6 a7 a8).



Definition mkMat_3_3' (a11 a12 a13
                        a21 a22 a23
                        a31 a32 a33 :A) :=
  [[a11;a12;a13];
   [a21;a22;a23];
   [a31;a32;a33]].


Definition cond2_mkMat_3_3':
  forall a11 a12 a13 a21 a22 a23 a31 a32 a33,
  width (mkMat_3_3' a11 a12 a13 a21 a22 a23 a31 a32 a33) 3%nat.
Proof. simpl. auto. Qed.

Definition mkMat_3_3 (a11 a12 a13
                        a21 a22 a23
                        a31 a32 a33 :A):=
  mkMat A 3 3 (mkMat_3_3' a11 a12 a13 a21 a22 a23 a31 a32 a33)
  eq_refl
  (cond2_mkMat_3_3' a11 a12 a13 a21 a22 a23 a31 a32 a33).

End Mat_make.
Arguments mkMat_dl {A} {m0}{n0}.
Arguments mkMat_1_1 {A}.
Arguments mkMat_1_2 {A}.
Arguments mkMat_2_1 {A}.
Arguments mkMat_2_2 {A}.
Arguments mkMat_2_4 {A}.
Arguments mkMat_3_3 {A}.

